$\forall$$A$, $B$:Type, ${\it eq}_{1}$:EqDecider($A$), ${\it eq}_{2}$:EqDecider($B$), $L$:($A$$\times$$B$) List.
\\[0ex]no\_repeats($A$;fpf{-}domain(fpf($L$)))
\\[0ex]\& ($\forall$$a$:$A$. ($a$ $\in$ fpf{-}domain(fpf($L$))) $\Leftrightarrow$ ($\exists$$b$:$B$. ($\langle$$a$$,\,$$b$$\rangle$ $\in$ $L$)))
\\[0ex]\& $\forall$$a$$\in$dom(fpf($L$)). $l$=fpf($L$)($a$) $\Rightarrow$  no\_repeats($B$;$l$) \& ($\forall$$b$:$B$. ($b$ $\in$ $l$) $\Leftrightarrow$ ($\langle$$a$$,\,$$b$$\rangle$ $\in$ $L$))